Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		minus(n__0,Y)	→ 0
2:		minus(n__s(X),n__s(Y))	→ minus(activate(X),activate(Y))
3:		geq(X,n__0)	→ true
4:		geq(n__0,n__s(Y))	→ false
5:		geq(n__s(X),n__s(Y))	→ geq(activate(X),activate(Y))
6:		div(0,n__s(Y))	→ 0
7:		div(s(X),n__s(Y))	→ if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0)
8:		if(true,X,Y)	→ activate(X)
9:		if(false,X,Y)	→ activate(Y)
10:		0	→ n__0
11:		s(X)	→ n__s(X)
12:		activate(n__0)	→ 0
13:		activate(n__s(X))	→ s(X)
14:		activate(X)	→ X

There are 16 dependency pairs:


15:		MINUS(n__0,Y)	→ 0#
16:		MINUS(n__s(X),n__s(Y))	→ MINUS(activate(X),activate(Y))
17:		MINUS(n__s(X),n__s(Y))	→ ACTIVATE(X)
18:		MINUS(n__s(X),n__s(Y))	→ ACTIVATE(Y)
19:		GEQ(n__s(X),n__s(Y))	→ GEQ(activate(X),activate(Y))
20:		GEQ(n__s(X),n__s(Y))	→ ACTIVATE(X)
21:		GEQ(n__s(X),n__s(Y))	→ ACTIVATE(Y)
22:		DIV(s(X),n__s(Y))	→ IF(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0)
23:		DIV(s(X),n__s(Y))	→ GEQ(X,activate(Y))
24:		DIV(s(X),n__s(Y))	→ DIV(minus(X,activate(Y)),n__s(activate(Y)))
25:		DIV(s(X),n__s(Y))	→ MINUS(X,activate(Y))
26:		DIV(s(X),n__s(Y))	→ ACTIVATE(Y)
27:		IF(true,X,Y)	→ ACTIVATE(X)
28:		IF(false,X,Y)	→ ACTIVATE(Y)
29:		ACTIVATE(n__0)	→ 0#
30:		ACTIVATE(n__s(X))	→ S(X)

The approximated dependency graph contains 3 SCCs: {19}, {16} and {24}.

Consider the SCC {19}. The usable rules are {10-14}. By taking the AF π with π(activate) = π(GEQ) = 1 together with the lexicographic path order with precedence n__0 ≈ 0 and n__s ≈ s, the rules in {10-14} are weakly decreasing and rule 19 is strictly decreasing.

Consider the SCC {16}. The usable rules are {10-14}. By taking the AF π with π(activate) = π(MINUS) = 1 together with the lexicographic path order with precedence n__0 ≈ 0 and n__s ≈ s, the rules in {10-14} are weakly decreasing and rule 16 is strictly decreasing.

Consider the SCC {24}. The usable rules are {1,2,10-14}. By taking the AF π with π(activate) = π(DIV) = 1 and π(minus) = π(n__s) = π(s) = [ ] together with the lexicographic path order with precedence n__s ≻ minus ≻ n__0, n__0 ≈ 0 and n__s ≈ s, the rules in {2,10-14} are weakly decreasing and the rules in {1,24} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.15 seconds) --- May 4, 2006